/* 
 * Copyright 2014 Josef Hertl.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package caetus.modelChecking.role;

import caetus.modelChecking.variable.ModelVariable;
import caetus.modelChecking.variable.ModelVariableTypeComparator;
import caetus.pkcs11.tokenCapabilities.TokenCapabilities;
import java.util.Collections;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.TreeMap;

/**
 * Represents a role in a model for model-checking. Splits into subclasses that
 * define behavior.
 *
 * @author Josef Hertl
 */
public abstract class ModelRole {

    protected String name;
    protected List<ModelVariable> localVariables = new LinkedList<ModelVariable>();
    protected List<ModelVariable> globalVariables = new LinkedList<ModelVariable>();
    /**
     * Variables that are only used to generate attached boolean variables such
     * as canWrap or canDecrypt
     */
    protected List<ModelVariable> hiddenVariables = new LinkedList<ModelVariable>();
    protected TokenCapabilities capabilities;

    public ModelRole(String name, TokenCapabilities capabilities) {
        this.name = name;
        this.capabilities = capabilities;
    }

    /**
     * @return Name of the role.
     */
    public String getName() {
        return name;
    }

    /**
     * completely prepares the role for the hlpsl specification.
     *
     * @return hlpsl-ready representation of the role.
     */
    public abstract String makeRole();

    /**
     * Prepares init - currently used for the preshared private key.
     *
     * @return hlpsl-ready form of init
     */
    protected abstract String prepareInit();

    /**
     * @return Text shown at a start of every role including Environment.
     */
    protected String makeRoleStart() {
        String result = "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n";
        result += "role " + name + "\n";
        result += prepareGlobalVariables();
        return result;
    }

    /**
     * @return The text that is added at an end of every role.
     */
    protected String makeRoleEnd() {
        return "\nend role\n\n";
    }

    /**
     * @return hlpsl-ready string that contains the hlpsl representation of
     * global variables.
     */
    protected String prepareGlobalVariables() {
        return "(" + prepareVariableHLPSL(globalVariables) + ")\n";
    }

    /**
     * @return hlpsl-ready string representation of local variables, including
     * the keyword "local"
     */
    protected String prepareLocalVariables() {
        return "local\n" + prepareVariableHLPSL(localVariables) + "\n";
    }

    /**
     * @return hlpsl-ready string representation of constants in the
     * environment.
     */
    protected String prepareConstants(List<ModelVariable> inputList) {
        return "const\n" + prepareVariableHLPSL(inputList, true);
    }

    /**
     *
     * @param inputList the list from which the hlpsl should be made.
     * @return hlpsl-ready list of the variables that can be later used for
     * either global or local variables.
     */
    private String prepareVariableHLPSL(List<ModelVariable> inputList) {
        return prepareVariableHLPSL(inputList, false);
    }

    /**
     *
     * @param inputList the list from which the hlpsl should be made.
     * @return hlpsl-ready list of the variables that can be later used for
     * either global or local variables.
     */
    private String prepareVariableHLPSL(List<ModelVariable> inputList, boolean toLowerCase) {
        Map<String, List<ModelVariable>> inputMap = new TreeMap<String, List<ModelVariable>>(new ModelVariableTypeComparator());
        //first the list is sorted according to the variable types. Since there may be more complex variables, this complicated approach must be used.
        for (ModelVariable modelVariable : inputList) {
            if (inputMap.get(modelVariable.getVariableType()) == null) {
                inputMap.put(modelVariable.getVariableType(), new LinkedList<ModelVariable>());
            }
            inputMap.get(modelVariable.getVariableType()).add(modelVariable);
        }
        String result = "";
        int amountFinished = 0; //variable used to keep count so that we know if we have to add , behind the row
        for (String typeString : inputMap.keySet()) {
            List<ModelVariable> rowVariablesList = inputMap.get(typeString);
            result += "	";
            for (int i = 0; i < rowVariablesList.size(); i++) {
                if (toLowerCase) {
                    result += rowVariablesList.get(i).getVariableName().toLowerCase();
                } else {
                    result += rowVariablesList.get(i).getVariableName();
                }
                if (i < (rowVariablesList.size() - 1)) {
                    result += ",";
                }
            }
            result += " : " + typeString;
            amountFinished++;
            if (amountFinished < inputMap.keySet().size()) {
                result += ",\n";
            }
        }
        return result;
    }

    /**
     * Adds all the elements from inputList to the global variables of this role
     */
    public void addToGlobalVariables(List<ModelVariable> inputList) {
        globalVariables.addAll(inputList);
        Collections.sort(globalVariables);
    }

    /**
     * Adds the given variable to the global variables of this role
     */
    public void addGlobalVariable(ModelVariable variable) {
        globalVariables.add(variable);
        Collections.sort(globalVariables);
    }

    /**
     * Adds all the elements from inputList to the local variables of this role
     */
    public void addToLocalVariables(List<ModelVariable> inputList) {
        localVariables.addAll(inputList);
        Collections.sort(localVariables);
    }

    /**
     * Adds the given variable to the local variables of this role
     */
    public void addLocalVariable(ModelVariable variable) {
        localVariables.add(variable);
        Collections.sort(localVariables);
    }

    /**
     * Finds the required local variable. Looks in both local and global
     * variables. Searches local variables first.
     *
     * @param name The name of the variable.
     * @return The looked-for variable. Null if such variable does not exist.
     */
    protected ModelVariable findVariable(String name) {
        for (ModelVariable modelVariable : localVariables) {
            if (modelVariable.getVariableName().equals(name)) {
                return modelVariable;
            }
        }
        for (ModelVariable modelVariable : globalVariables) {
            if (modelVariable.getVariableName().equals(name)) {
                return modelVariable;
            }
        }
        return null;
    }

    public List<ModelVariable> getGlobalVariables() {
        return Collections.unmodifiableList(globalVariables);
    }

    /**
     * @return List of variables that are declared with the keyword local.
     */
    public List<ModelVariable> getLocalVariables() {
        return Collections.unmodifiableList(localVariables);
    }
}
